D:Dsys, i:Id. {m:M(i).Msg| source(mlnk(m)) = i}  r Msg(l,tg. M(source(l)).dout(l,tg)) 

latex

Definitions	x:A. B(x), t  T, Msg(M), M.Msg, Msg(da), mlnk(m), t.1, M.dout(l,tg)
Lemmas	ma-msg wf, d-m wf, lsrc wf, mlnk wf d, Msg wf, ma-dout wf, IdLnk wf, Id wf, dsys wf, subtype rel self